package probsym;
public class LattECounterTests {
	
	/**
	 * There are two paths.  Assuming integer domain of 0..9 here are the counts:
	 *    y == x+z : 55
	 *    y != x+z : 945
	 */
	public static void testEqualities1(int x, int y, int z) {	
		if (y == x + z) {
			x = 1;
		}
	}

	/**
	 * There are 6 (sub) paths.  Assuming integer domain of 0..9 here are the counts:
	 *   y==7 : 1
	 *   y!=7 : 9
	 *   y==7 & z==y : 1
	 *   y==7 & z!=y : 9
	 *   y!=7 & z==y : 9
	 *   y!=7 & z!=y : 81
	 *   
	 * NB: these are the counts reported by LattECounter which only is given the 
	 *     relevant fragment of the constraint (it doens't know about z and x in
	 *     the first case, for example)
	 */
	public static void testEqualities2(int x, int y, int z) {	
		if (y == 7) {
			x = 1;
		}
		if (z == y) {
			z = 1;
		}
	}
	
	/**
	 * This example really gets into the combinatorics of multiple disequalities. 
	 * Here are all of the sub-paths and the resulting LattE constraints.  The
	 * cache HITs are denoted, but remember that it depends on the order in which
	 * contraints are explored.
	 * 
	 *   x==y : 10
	 *   
	 *   x!=y : 90
	 *   
	 *   x==y & x!=0 => 
	 *       x==y :  HIT
	 *       x==y & x==0 : 1
	 *       
	 *   x==y & x==0 : HIT
	 *   
	 *   x==y & x!=0 & y!=1 => 
	 *       x==y : HIT
	 *       x==y & x==0 : HIT
	 *       x==y & y==1 : 1
	 *       x==y & x==0 & y==1 : 0
	 *       
	 *   x==y & x!=0 & y==1 => 
	 *       x==y & y==1 : HIT
	 *       x==y & y==1 & x==0 : HIT
	 *       
	 *   x==y & x!=0 & y!=1 & x!=2 =>
	 *       x==y : HIT
	 *       x==y & x==0 : HIT
	 *       x==y & y==1 : HIT
	 *       x==y & x==2 : 1
	 *       x==y & x==0 & y==1 : HIT
	 *       x==y & x==0 & x==2 : 0
	 *       x==y & y==1 & x==2 : 0
	 *       x==y & x==0 & y==1 & x==2 : 0
	 *       
	 *   x==y & x!=0 & y!=1 & x==2 =>
	 *       x==y & x==2 : HIT
	 *       x==y & x==2 & x==0 : HIT
	 *       x==y & x==2 & y==1 : HIT
	 *       x==y & x==2 & x==0 & y==1 : HIT
	 *       
	 *   x==y & x!=0 & y!=1 & x!=2 & y!=3 =>
	 *       x==y : HIT
	 *       x==y & x==0 : HIT
	 *       x==y & y==1 : HIT
	 *       x==y & x==2 : HIT
	 *       x==y & y==3 : 1
	 *       x==y & x==0 & y==1 : HIT
	 *       x==y & x==0 & x==2 : HIT
	 *       x==y & x==0 & y==3 : 0
	 *       x==y & y==1 & x==2 : HIT
	 *       x==y & y==1 & y==3 : 0
	 *       x==y & x==2 & y==3 : 0
	 *       x==y & x==0 & y==1 & x==2 : HIT
	 *       x==y & x==0 & y==1 & y==3 : 0
	 *       x==y & x==0 & x==2 & y==3 : 0
	 *       x==y & y==1 & x==2 & y==3 : 0
	 *       x==y & x==0 & y==1 & x==2 & y==3 : 0
	 *       
	 *   x==y & x!=0 & y!=1 & x!=2 & y==3
	 *       x==y & y==3 : HIT
	 *       x==y & y==3 & x==0 : HIT
	 *       x==y & y==3 & y==1 : HIT
	 *       x==y & y==3 & x==2 : HIT
	 *       x==y & y==3 & x==0 & y==1 : HIT
	 *       x==y & y==3 & x==0 & x==2 : HIT
	 *       x==y & y==3 & y==1 & x==2 : HIT
	 *       x==y & y==3 & x==0 & y==1 & y==3 : HIT
	 *       
	 *  This should result in 17 calls and 30 cache hits.
	 *       
	 */
	public static void testLotsOfDisequalities(int x, int y, int z) {	
		if (x == y) {
			if (x != 0) {
				if (y != 1) {
					if (x != 2) {
						if (y != 3) {
							z = 1;
						}
					}
				}
			}
		}
	}

	
	/**
	 * There are 6 (sub) paths.  Assuming integer domain of 0..9 here are the counts:
	 *     x<=0 : 1
	 *     x>0 : 9
	 * the remaining 4 sub paths are all reduced and result in cache hits.
	 *      
	 * NB: these are the counts reported by LattECounter which only is given the 
	 *     relevant fragment of the constraint (it doens't know about z and x in
	 *     the first case, for example)
	 */
	public static void testNoEqualities(int x, int y, int z) {
		if (x > 0) {
			if (y > 0) {
				if (z > 0) {
					x = 1;
				}
			}
		}
	}
	
	public static void testMore(int x, int y, int z) {
		if (2*x > y - 2) {
			z = 1;
		}
		
		if (y < 5) {
			x = y;
		}
		
		if (y == 0) {
			x = 1;
		}
		if (z == y) {
			z = 1;
		}
		
	}
	
	/**
	 * Test that symmetry up to renaming works.  Should see:
	 *     6 calls and 4 cache hits
	 * without canonization, but 4 calls and 6 cache hits with.
	 */
	public static void testCacheRenaming(int x, int y, int z) {
		if (x > 0) {
			if (y > 0) {
				if (z < y) {
					y = 1;
				}
			}
		} else {
			if (z > 0) {
				if (y < z) {
					z = 1;
				}
			}
		}
	}
	
	/**
	 * Test that symmetry up to renaming works.  Should see:
	 *     6 calls and 4 cache hits
	 * without canonization, but 4 calls and 6 cache hits with.
	 */
	public static void testCacheReorder(int x, int y, int z) {
		if (x > 0) {
			if (y > 0) {
				if (z < y) {
					y = 1;
				}
			}
		} else {
			if (z > y) {
				if (0 < z) {
					z = 1;
				}
			}
		}
	}

	/**
	 * Assuming that the integer domain is 0..9 (10 values)
	 * We should have two constraint combinations:
	 *   x > y : count 45, Prob(0.45)
	 *   x <= y : count 55, Prob(0.55)
	 */
	public static void testDiagonal(int x, int y) {
		if (x > y) {
			y = 1;
		}
	}
	
	/**
	 * Assuming that the integer domain is 0..9 (10 values in domain)
	 * We should have four constraint combinations
	 *   x > 5 : count should be 4, Prob(0.4)
	 *   x <= 5 : count should be 6, Prob(0.6)
	 *   x > 5 & x < 7 : count should be 1, Prob(0.1)
	 *   x > 5 & x >= 7 : count should be 3, Prob(0.3)
	 */
	public static void testInterval(int x) {
		if (x > 5) {
			if (x < 7) {
				x = 1;
			}
		}
	}

	public static int m(int x, int y) {
		if (x<0) x = -x;   
		  if (y<0) y = -y;
		  if (x<10) {
		    return 1;
		  } else if (9<y) {
		    return -1;
		  } else {
		    return 0;
		  }
		}

	public static void main(String[] args) {
		m(5,5);
		//testEqualities1(20, 10, 5);
		//testEqualities2(20, 10, 5);
		//testLotsOfDisequalities(20, 10, 5);
		//testNoEqualities(20, 10, 5);
		//testMore(20, 10, 5);
		//testDiagonal(20, 10);
		//testInterval(20);
		//testCacheRenaming(20, 10, 5);
		//testCacheReorder(20, 10, 5);
	}


}
